In recent years, the functionality of random access memories (RAMs) disposed inside or outside large scale integrations (LSIs) has increased. As the circuit scale of RAMs has increased, the logic configuration has become more complicated. Accordingly, the difficulty of logic verification of such RAMs with increased functionality is increasing and, therefore, it is required that logic verification is performed correctly and efficiently. In order to satisfy such a demand, the following method for verifying a logic circuit, for example, has been developed. That is, signal transition information used when logic is verified in a behavior level is used as an input vector and output expectation values in transistor-level logic verification (refer to, for example, Naoshi HIGAKI et al., “Design Methodology for Low-Power-Consumption RAM IP” Magazine Fujitsu, FUJITSU limited, January 2002, pp. 40-46).
The following three methods for testing functional equivalence are currently available to designers: logic simulation, cone-based equivalence checking, and symbolic simulation.
In logic simulation, an ideal model of a logic circuit to be realized, that is, a reference model, is written in the register transfer level (RTL) having an abstraction level higher than the gate level. In addition, implementation of an actually designed logic circuit is written using a gate-level netlist or a transistor-level netlist. Furthermore, a variety of input signals are given to the reference model and the implementation. It is then determined that the logic circuit of the implementation is correct if the output signals output from the reference model and the implementation are the same.
In this method, only a limitation that the input and output terminals of the reference model and the implementation need to be the same is required. Thus, this method is applicable to a wide variety of applications. However, in order to completely verify the logic circuit, all of the possible input signals need to be given to the reference model and the implementation. Accordingly, as the number of input signals increases, the number of combinations of the input signals significantly increases. As a result, it is difficult to completely verify the logic circuit.
In cone-based equivalence checking, a reference and an implementation are separated into logic cones representing logic groups having boundaries, such as memory elements and input and output (I/O) ports. Thereafter, formal logic equivalence checking between the reference and the implementation is performed for each of the logic cones.
In the cone-based equivalence checking, all combinations of possible input signals are verified. Accordingly, complete checking can be realized. In addition, the efficiency of checking can be advantageously increased. However, since a synthesizable logic description model is required, this method is applicable to only combinational circuits. As a result, this method is not suitable for transistor-level design or design of a memory element having a large circuit scale.
Symbolic simulation is a combination of the two methods. In the logic simulation, a logical value, such as “0” or “1” is used as an input value. However, in the symbolic simulation, a symbol is used as an input value in place of a logical value. The logical value of a symbol is “0” or “1”. Accordingly, n symbols are input to n inputs (n: a natural number). Consequently, these n symbols represent 2n input signals (refer to, for example, Simon Napper, Dian Yang, “Equivalence Checking a 256 MB SDRAM”, Memory Technology, Design and Testing, IEEE International Workshop on 2002, August 2001, pp. 85-89, or Paul Hoxey et al., “An introduction to symbolic simulation”, Dec. 19, 2005, United Business Media LLC).
This method is based on simulation. Accordingly, unlike the cone-based equivalence checking, the application targets are not limited. However, generation of a test bench in accordance with a target design is required and, therefore, it is more difficult to generate such a test bench than a test bench used for logic simulation.
As mentioned earlier, the functionality and configuration of RAMs have become complicated. Accordingly, it is desirable that equivalence checking of a RAM be efficiently performed. In general, among the above-described three methods, the logic simulation or symbolic simulation is suitable for equivalence checking of a RAM having advanced functionalities. In particular, in recent years, symbolic simulation that can provide more efficient equivalence checking has garnered much attention.
However, since symbolic simulation is a new technology, available tools for symbolic simulation are costly. In addition, the number of types of tool is limited. Furthermore, in order to perform equivalence checking, a reference model needs to be generated. Still furthermore, a test bench needs to be generated for respective targets to be checked. However, in order to generate the models and test benches, additional skill is required, as compared with that for logic simulation. Still furthermore, since the target to be checked is limited to the target defined by the test bench, complete checking is difficult.
Accordingly, it is desirable that symbolic simulation that requires a high cost and a high level of skill only be used for an area of a circuit that is as small as possible. For the other areas of the circuit, it is desirable that other equivalence checking that provides high work efficiency at lower cost be employed. In addition, such a requirement is not limited to RAMs, but widely arises for other semiconductor memories, such as read only memories (ROMs) and semiconductor circuits having a large-scale logic configuration with regularity.